| Definitions | f(x), x : v,  T, isl(x), Y, reduce(f;k;as), deq-member(eq;x;L), mk-ma, Top, rcv(l,tg), with declarations ds:dsda:dak(v) sends f s v on link l, with declarations ds:dsda:daeffect of k(v) is x := f s v, , rcv(l,tg) declared in M, M.din(l,tg), M.dout(l,tg), interface-link(A;B;l;tg), f(x)?z, isrcv(k), x  dom(f), t.2, t.1,  , True, tt, ff,   x. t(x), R-base-ma(R), @i: A, Rsends?(x1), Reffect?(x1), Rnone?(x1), R-loc(R), if b then t else f fi , Rplus?(x1),  b,  A, Dsys, case(R)Rnone: noneleft  right: comb(left;right)base(b). base(b), ,  , {T}, SQType(T), t T, P & Q, [[R]], interface-compatible(A;B), P   Q,  x:A. B(x), tag(k), let x = a in b(x), outl(x), Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), lnk(k), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), p   q, (i = j), p  q, x(s),  , Unit, R-interface-compat(A;B), R-frame-compat(A;B), R-base-domain(R), p = q, Rda(R), Rds(R), R-Feasible(R), Realizer, Dec(P), False, P  Q, P Q, A || B, a = b, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left right, Rnone(),  |
| Lemmas | fpf-ap wf, IdLnk sq, squash wf, Id sq, assert-eq-lnk, eq lnk wf, lnk-decl-cap2, assert-eq-knd, eq knd wf, fpf-cap-single, fpf-join-cap, Rsends wf, fpf-trivial-subtype-top, lnk-decl wf, fpf-join wf, true wf, Reffect wf, R-interface-compat wf, R-discrete compat wf, R-frame-compat wf, Rda wf, Rds wf, id-deq wf, fpf-compatible wf, R-base-domain wf, eq bd wf, fpf-cap-single1, Knd sq, fpf-single-dom, not functionality wrt iff, rcv wf, top wf, fpf-single wf, Kind-deq wf, fpf-dom wf, assert-eq-id, eq id wf, false wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, Knd wf, rationals wf, unit wf, es realizer wf, Rplus? wf, R-Feasible wf, R-compat wf, IdLnk wf, lsrc wf, R-base-ma wf, R-loc wf, m-sys-at wf2, interface-link wf, ldst wf, ma-declm-R-base-ma, decidable assert, Rsends? wf, Reffect? wf, decidable or, R-Dsys-base, not wf, interface-compatible-null, Id wf, ma-empty wf, R-Dsys wf, interface-compatible-symmetry, Rnone-implies, Rnone? wf, assert of bnot, eqff to assert, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, bool sq, bool cases |